Introduction - Syllabus overview
Foundations of logics and proofs
Proof using TT, DeMorgan's laws
Satisfiability of propositional formulas
Validity of formula - Interpretations
Satisfiability of formulas - theorems and proofs
Satisfiability using semantic tableaux
Analysis of satisfiability using semantic tableaux
Properties of decision procedures
Soundness and completeness
Hintikka set
Hintikka's lemma - proof
Ground Resolution Rule
DP Algorithm
Satisfiability using semantic tableaux - problems
Partial Interpretation
DPLL algorithm
Revision of Unit-1 portions
N-queens problem
N-queens problem- contd
Deductive systems for PL - Gentzen system
Gentzen system
Hilbert system
Skolem's algorithm
Skolem's algorithm
First order Logic - basics
First order Logic - interpretations
FOL - Herbrand model
Substitution - Composition
General Resolution Procedure
Soundness of resolution
Lifting Lemma - Proof
Temporal logic
Operators of PTL
State transition diagrams
Deductive system - L for temporal logic
Hoare logic
Scheduling algorithms
Correctness of concurrent programs
Lambda calculus - introduction
Parenthesization
Free, bound and binding variables
Substitution in lambda
Substitution - problems
Substitution - problems
Substitution - Lemma and proof
Beta reduction
Beta reduction
Beta equality
Beta equality - problems
Combinatory logic - introduction
Substitution in CL
Substitution in CL - problems
Reduction in CL
Reduction in CL - problems
Reduction in CL - problems
Lambda and combinators - fixed point theorem
Primitive recursive functions
